$\forall$${\it the\_es}$:ES. SWellFounded(($x$ $<$loc $y$))